Inference at * 
Iof proof for Lemma lt to le rw:


  i, j:. {(i < j)  ((i+1)  j)} 

latex

 by ((Unfold `guard` 0) 
CollapseTHEN (Lemma `lt_to_le`)) 

latex

C.

Definitions	{T}
Lemmas	lt to le